<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Perm: Basic Techniques for Permutations and Ordering</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: Verified Functional Algorithms</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Perm<span class="subtitle">Basic Techniques for Permutations and Ordering</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 Consider these algorithms and data structures:

<div class="paragraph"> </div>

<ul class="doclist">
<li> sort a sequence of numbers;

</li>
<li> finite maps from numbers to (arbitrary-type) data

</li>
<li> finite maps from any ordered type to (arbitrary-type) data

</li>
<li> priority queues: finding/deleting the highest number in a set

</li>
</ul>
 To prove the correctness of such programs, we need to reason
 about less-than comparisons (for example, on integers) and about
 "these two sets/sequences have the same contents".  In this
 chapter, we introduce some techniques for reasoning about:

<div class="paragraph"> </div>

<ul class="doclist">
<li> less-than comparisons on natural numbers

</li>
<li> permutations (rearrangements of lists)

</li>
</ul>
 Then, in later chapters, we'll apply these proof techniques
 to reasoning about algorithms and data structures.
 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Coq.Strings.String</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Bool.Bool</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Arith.Arith</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Arith.EqNat</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.omega.Omega</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Lists.List</span>.<br/>
<span class="id" type="keyword">Export</span> <span class="id" type="var">ListNotations</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Permutation</span>.<br/>
</div>

<div class="doc">
<a name="lab10"></a><h1 class="section">The Less-Than Order on the Natural Numbers</h1>

<div class="paragraph"> </div>

 These <span class="inlinecode"><span class="id" type="keyword">Check</span></span> and <span class="inlinecode"><span class="id" type="var">Locate</span></span> commands remind us about
  <i>Propositional</i> and the <i>Boolean</i> less-than operators
  in the Coq standard library. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">Nat.lt</span>. <span class="comment">(*&nbsp;:&nbsp;nat&nbsp;-&gt;&nbsp;nat&nbsp;-&gt;&nbsp;Prop&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">lt</span>. <span class="comment">(*&nbsp;:&nbsp;nat&nbsp;-&gt;&nbsp;nat&nbsp;-&gt;&nbsp;Prop&nbsp;*)</span><br/>
<span class="id" type="keyword">Goal</span> <span class="id" type="var">Nat.lt</span> = <span class="id" type="var">lt</span>. <span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>. <span class="comment">(*&nbsp;They&nbsp;are&nbsp;the&nbsp;same&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Nat.ltb</span>. <span class="comment">(*&nbsp;:&nbsp;nat&nbsp;-&gt;&nbsp;nat&nbsp;-&gt;&nbsp;bool&nbsp;*)</span><br/>
<span class="id" type="var">Locate</span> "_ &lt; _". <span class="comment">(*&nbsp;"x&nbsp;&lt;&nbsp;y"&nbsp;:=&nbsp;lt&nbsp;x&nbsp;y&nbsp;*)</span><br/>
<span class="id" type="var">Locate</span> "&lt;?". <span class="comment">(*&nbsp;x&nbsp;&lt;?&nbsp;y&nbsp;&nbsp;:=&nbsp;Nat.ltb&nbsp;x&nbsp;y&nbsp;*)</span><br/>
</div>

<div class="doc">
We write <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&lt;</span> <span class="inlinecode"><span class="id" type="var">y</span></span> for the Proposition that <span class="inlinecode"><span class="id" type="var">x</span></span> <i>is</i> less than <span class="inlinecode"><span class="id" type="var">y</span></span>,
    and we write <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&lt;?</span> <span class="inlinecode"><span class="id" type="var">y</span></span> for the computable <i>test</i> that returns
    <span class="inlinecode"><span class="id" type="var">true</span></span> or <span class="inlinecode"><span class="id" type="var">false</span></span> depending on whether <span class="inlinecode"><span class="id" type="var">x</span>&lt;<span class="id" type="var">y</span></span>.  The theorem that
    <span class="inlinecode"><span class="id" type="var">lt</span></span> is related in this way to <span class="inlinecode"><span class="id" type="var">ltb</span></span> is this one: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">Nat.ltb_lt</span>.<br/>
<span class="comment">(*&nbsp;:&nbsp;forall&nbsp;n&nbsp;m&nbsp;:&nbsp;nat,&nbsp;(n&nbsp;&lt;?&nbsp;m)&nbsp;=&nbsp;true&nbsp;&lt;-&gt;&nbsp;n&nbsp;&lt;&nbsp;m&nbsp;*)</span><br/>
</div>

<div class="doc">
For some reason, the Coq library has <span class="inlinecode"></span> <span class="inlinecode">&lt;?</span> <span class="inlinecode"></span> and <span class="inlinecode"></span> <span class="inlinecode">&lt;=?</span> <span class="inlinecode"></span>
    notations, but is missing these three: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span>  "a &gt;=? b" := (<span class="id" type="var">Nat.leb</span> <span class="id" type="var">b</span> <span class="id" type="var">a</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 70, <span class="id" type="var">only</span> <span class="id" type="var">parsing</span>) : <span class="id" type="var">nat_scope</span>.<br/>
<span class="id" type="keyword">Notation</span>  "a &gt;? b"  := (<span class="id" type="var">Nat.ltb</span> <span class="id" type="var">b</span> <span class="id" type="var">a</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 70, <span class="id" type="var">only</span> <span class="id" type="var">parsing</span>) : <span class="id" type="var">nat_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> " a =? b"  := (<span class="id" type="var">beq_nat</span> <span class="id" type="var">a</span> <span class="id" type="var">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 70) : <span class="id" type="var">nat_scope</span>.<br/>
</div>

<div class="doc">
<a name="lab11"></a><h2 class="section">Relating <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> to <span class="inlinecode"><span class="id" type="var">bool</span></span></h2>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">reflect</span></span> relation connects a <span class="inlinecode"><span class="id" type="var">Proposition</span></span> to a <span class="inlinecode"><span class="id" type="var">Boolean</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">reflect</span>.<br/>
</div>

<div class="doc">
That is, <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> means that <span class="inlinecode"><span class="id" type="var">P</span>↔<span class="id" type="var">True</span></span> if and only if <span class="inlinecode"><span class="id" type="var">b</span>=<span class="id" type="var">true</span></span>.
     The way to use <span class="inlinecode"><span class="id" type="var">reflect</span></span> is, for each of your operators, make a
     lemma like these next three:

</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">beq_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">x</span> = <span class="id" type="var">y</span>) (<span class="id" type="var">x</span> =? <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">beq_nat_true_iff</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">blt_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">x</span> &lt; <span class="id" type="var">y</span>) (<span class="id" type="var">x</span> &lt;? <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Nat.ltb_lt</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ble_reflect</span> : <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">x</span> ≤ <span class="id" type="var">y</span>) (<span class="id" type="var">x</span> &lt;=? <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Nat.leb_le</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here's an example of how you could use these lemmas.
    Suppose you have this simple program, <span class="inlinecode">(<span class="id" type="keyword">if</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">&lt;?</span> <span class="inlinecode">5</span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode">2)</span>,
    and you want to prove that it evaluates to a number smaller than 6.
    You can use <span class="inlinecode"><span class="id" type="var">blt_reflect</span></span> "by hand": 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reflect_example1</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">a</span>, (<span class="id" type="keyword">if</span> <span class="id" type="var">a</span>&lt;?5 <span class="id" type="keyword">then</span> <span class="id" type="var">a</span> <span class="id" type="keyword">else</span> 2) &lt; 6.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">blt_reflect</span> <span class="id" type="var">a</span> 5) <span class="id" type="keyword">as</span> [<span class="id" type="var">H</span>|<span class="id" type="var">H</span>].<br/>
&nbsp;&nbsp;* <span class="comment">(*&nbsp;Notice&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;above&nbsp;the&nbsp;line&nbsp;has&nbsp;a&nbsp;<span class="inlinecode"><span class="id" type="keyword">Prop</span></span>ositional<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;fact&nbsp;_related_&nbsp;to&nbsp;<span class="inlinecode"><span class="id" type="var">a</span>&lt;?5</span>*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">omega</span>. <span class="comment">(*&nbsp;More&nbsp;explanation&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>&nbsp;later&nbsp;in&nbsp;this&nbsp;chapter.&nbsp;*)</span><br/>
&nbsp;&nbsp;* <span class="comment">(*&nbsp;Notice&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;above&nbsp;the&nbsp;line&nbsp;has&nbsp;a&nbsp;a&nbsp;_different_<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="keyword">Prop</span></span>ositional&nbsp;fact.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_lt</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="comment">(*&nbsp;This&nbsp;step&nbsp;is&nbsp;not&nbsp;necessary,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;it&nbsp;just&nbsp;makes&nbsp;the&nbsp;hypothesis&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;look&nbsp;pretty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
But there's another way to use <span class="inlinecode"><span class="id" type="var">blt_reflect</span></span>, etc: read on. 
<div class="paragraph"> </div>

<a name="lab12"></a><h2 class="section">Some Advanced Tactical Hacking</h2>
 You may skip ahead to "Inversion/clear/subst".
     Right here, we build some machinery that you'll want to
     <i>use</i>, but you won't need to know how to <i>build</i> it.

<div class="paragraph"> </div>

    Let's put several of these <span class="inlinecode"><span class="id" type="var">reflect</span></span> lemmas into a Hint database,
    called <span class="inlinecode"><span class="id" type="var">bdestruct</span></span> because we'll use it in our boolean-destruction
    tactic: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">blt_reflect</span> <span class="id" type="var">ble_reflect</span> <span class="id" type="var">beq_reflect</span> : <span class="id" type="var">bdestruct</span>.<br/>
</div>

<div class="doc">
Our high-tech <i>boolean destruction</i> tactic: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Ltac</span> <span class="id" type="var">bdestruct</span> <span class="id" type="var">X</span> :=<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
&nbsp;&nbsp;<span class="id" type="keyword">let</span> <span class="id" type="var">H</span> := <span class="id" type="tactic">fresh</span> <span class="id" type="keyword">in</span> <span class="id" type="keyword">let</span> <span class="id" type="var">e</span> := <span class="id" type="tactic">fresh</span> "e" <span class="id" type="keyword">in</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">evar</span> (<span class="id" type="var">e</span>: <span class="id" type="keyword">Prop</span>);<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H</span>: <span class="id" type="var">reflect</span> <span class="id" type="var">e</span> <span class="id" type="var">X</span>); <span class="id" type="tactic">subst</span> <span class="id" type="var">e</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="tactic">eauto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">bdestruct</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">H</span>|<span class="id" type="var">H</span>];<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ | <span class="id" type="tactic">try</span> <span class="id" type="var">first</span> [<span class="id" type="tactic">apply</span> <span class="id" type="var">not_lt</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span> | <span class="id" type="tactic">apply</span> <span class="id" type="var">not_le</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>]]].<br/>
</div>
</div>

<div class="doc">
Here's a brief example of how to use <span class="inlinecode"><span class="id" type="var">bdestruct</span></span>.  There
     are more examples later. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reflect_example2</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">a</span>, (<span class="id" type="keyword">if</span> <span class="id" type="var">a</span>&lt;?5 <span class="id" type="keyword">then</span> <span class="id" type="var">a</span> <span class="id" type="keyword">else</span> 2) &lt; 6.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">a</span>&lt;?5). <span class="comment">(*&nbsp;instead&nbsp;of:&nbsp;<span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" type="var">blt_reflect</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">5)</span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode">[<span class="id" type="var">H</span>|<span class="id" type="var">H</span>]</span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;* <span class="comment">(*&nbsp;Notice&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;above&nbsp;the&nbsp;line&nbsp;has&nbsp;a&nbsp;<span class="inlinecode"><span class="id" type="keyword">Prop</span></span>ositional<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;fact&nbsp;_related_&nbsp;to&nbsp;<span class="inlinecode"><span class="id" type="var">a</span>&lt;?5</span>*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">omega</span>. <span class="comment">(*&nbsp;More&nbsp;explanation&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>&nbsp;later&nbsp;in&nbsp;this&nbsp;chapter.&nbsp;*)</span><br/>
&nbsp;&nbsp;* <span class="comment">(*&nbsp;Notice&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;above&nbsp;the&nbsp;line&nbsp;has&nbsp;a&nbsp;a&nbsp;_different_<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="keyword">Prop</span></span>ositional&nbsp;fact.&nbsp;We&nbsp;don't&nbsp;need&nbsp;to&nbsp;apply&nbsp;<span class="inlinecode"><span class="id" type="var">not_lt</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;as&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span>&nbsp;has&nbsp;already&nbsp;done&nbsp;it.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab13"></a><h2 class="section"><span class="inlinecode"><span class="id" type="tactic">inversion</span></span> / <span class="inlinecode"><span class="id" type="tactic">clear</span></span> / <span class="inlinecode"><span class="id" type="tactic">subst</span></span></h2>
 Coq's <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> tactic is so good at extracting information
    from the hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span> that <span class="inlinecode"><span class="id" type="var">H</span></span> becomes completely redundant,
    and one might as well <span class="inlinecode"><span class="id" type="tactic">clear</span></span> it from the goal.  Then, since the
    <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> typically creates some equality facts, why not then
    <span class="inlinecode"><span class="id" type="tactic">subst</span></span> ?   This motivates the following useful tactic, <span class="inlinecode"><span class="id" type="var">inv</span></span>:  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Ltac</span> <span class="id" type="var">inv</span> <span class="id" type="var">H</span> := <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
</div>

<div class="doc">
<a name="lab14"></a><h2 class="section">Linear Integer Inequalities</h2>

<div class="paragraph"> </div>

 In our proofs about searching and sorting algorithms, we
    sometimes have to reason about the consequences of
    less-than and greater-than.  Here's a contrived example. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Exploration1</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">omega_example1</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">i</span> <span class="id" type="var">j</span> <span class="id" type="var">k</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">i</span> &lt; <span class="id" type="var">j</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;¬ (<span class="id" type="var">k</span> - 3 ≤ <span class="id" type="var">j</span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">k</span> &gt; <span class="id" type="var">i</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
</div>

<div class="doc">
Now, there's a hard way to prove this, and an easy way.
    Here's the hard way. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="comment">(*&nbsp;try&nbsp;to&nbsp;remember&nbsp;the&nbsp;name&nbsp;of&nbsp;the&nbsp;lemma&nbsp;about&nbsp;negation&nbsp;and&nbsp;<span class="inlinecode">≤</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">Search</span> (¬ <span class="id" type="var">_</span> ≤ <span class="id" type="var">_</span> → <span class="id" type="var">_</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_le</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;try&nbsp;to&nbsp;remember&nbsp;the&nbsp;name&nbsp;of&nbsp;the&nbsp;transitivity&nbsp;lemma&nbsp;about&nbsp;<span class="inlinecode">&gt;</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">Search</span> (<span class="id" type="var">_</span> &gt; <span class="id" type="var">_</span> → <span class="id" type="var">_</span> &gt; <span class="id" type="var">_</span> → <span class="id" type="var">_</span> &gt; <span class="id" type="var">_</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">gt_trans</span> <span class="id" type="keyword">with</span> <span class="id" type="var">j</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">gt_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">k</span>-3).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;_OBVIOUSLY_,&nbsp;<span class="inlinecode"><span class="id" type="var">k</span></span>&nbsp;is&nbsp;greater&nbsp;than&nbsp;<span class="inlinecode"><span class="id" type="var">k</span>-3</span>.&nbsp;&nbsp;But&nbsp;_OOPS_,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;this&nbsp;is&nbsp;not&nbsp;actually&nbsp;true,&nbsp;because&nbsp;we&nbsp;are&nbsp;talking&nbsp;about<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;natural&nbsp;numbers&nbsp;with&nbsp;"bogus&nbsp;subtraction."&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">bogus_subtraction</span>: ¬ (<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">k</span>:<span class="id" type="var">nat</span>, <span class="id" type="var">k</span> &gt; <span class="id" type="var">k</span> - 3).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="tactic">intro</span></span>&nbsp;introduces&nbsp;exactly&nbsp;one&nbsp;thing,&nbsp;like&nbsp;<span class="inlinecode"><span class="id" type="tactic">intros</span></span> <span class="inlinecode">?</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intro</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="var">specialize</span></span>&nbsp;applies&nbsp;a&nbsp;hypothesis&nbsp;to&nbsp;an&nbsp;argument&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">specialize</span> (<span class="id" type="var">H</span> <span class="id" type="var">O</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
With bogus subtraction, this omega_example1 theorem even True?
    Yes it is; let's try again, the hard way, to find the proof. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">omega_example1</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">i</span> <span class="id" type="var">j</span> <span class="id" type="var">k</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">i</span> &lt; <span class="id" type="var">j</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;¬ (<span class="id" type="var">k</span> - 3 ≤ <span class="id" type="var">j</span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">k</span> &gt; <span class="id" type="var">i</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;try&nbsp;again!&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_le</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">gt</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">gt</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;try&nbsp;to&nbsp;remember&nbsp;the&nbsp;name&nbsp;...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">Search</span> (<span class="id" type="var">_</span> &lt; <span class="id" type="var">_</span> → <span class="id" type="var">_</span> ≤ <span class="id" type="var">_</span> → <span class="id" type="var">_</span> &lt; <span class="id" type="var">_</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">lt_le_trans</span> <span class="id" type="keyword">with</span> <span class="id" type="var">j</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">k</span>-3).<br/>
&nbsp;&nbsp;<span class="id" type="var">Search</span> (<span class="id" type="var">_</span> &lt; <span class="id" type="var">_</span> → <span class="id" type="var">_</span> ≤ <span class="id" type="var">_</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">lt_le_weak</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_minus</span>.<br/>
<span class="id" type="keyword">Qed</span>. <span class="comment">(*&nbsp;Oof!&nbsp;&nbsp;That&nbsp;was&nbsp;exhausting&nbsp;and&nbsp;tedious.&nbsp;&nbsp;*)</span><br/>
</div>

<div class="doc">
And here's the easy way. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">omega_example2</span>:<br/>
&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">i</span> <span class="id" type="var">j</span> <span class="id" type="var">k</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">i</span> &lt; <span class="id" type="var">j</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;¬ (<span class="id" type="var">k</span> - 3 ≤ <span class="id" type="var">j</span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">k</span> &gt; <span class="id" type="var">i</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here we have used the <span class="inlinecode"><span class="id" type="tactic">omega</span></span> tactic, made available by importing
    <span class="inlinecode"><span class="id" type="var">Coq.omega.Omega</span></span> as we have done above.  Omega is an algorithm
    for integer linear programming, invented in 1991 by William Pugh.
    Because ILP is NP-complete, we might expect that this algorithm is
    exponential-time in the worst case, and indeed that's true: if you
    have <span class="inlinecode"><span class="id" type="var">N</span></span> equations, it could take <span class="inlinecode">2^<span class="id" type="var">N</span></span> time.  But in the typical
    cases that result from reasoning about programs, omega is much
    faster than that.  Coq's <span class="inlinecode"><span class="id" type="tactic">omega</span></span> tactic is an implementation of
    this algorithm that generates a machine-checkable Coq proof.  It
    "understands" the types Z and nat, and these operators: <span class="inlinecode">&lt;</span> <span class="inlinecode">=</span> <span class="inlinecode">&gt;</span> <span class="inlinecode">≤</span>
    <span class="inlinecode">≥</span> <span class="inlinecode">+</span> <span class="inlinecode">-</span> <span class="inlinecode">¬</span>, as well as multiplication by small integer
    literals (such as 0,1,2,3...) and some uses of <span class="inlinecode">∨</span> and <span class="inlinecode">∧</span>.

<div class="paragraph"> </div>

    Omega does <i>not</i> understand other operators.  It treats things
    like <span class="inlinecode"><span class="id" type="var">a</span>*<span class="id" type="var">b</span></span> and <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> as if they were variables.  That is, it can
    prove <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode">&gt;</span> <span class="inlinecode"><span class="id" type="var">a</span>*<span class="id" type="var">b</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode">+</span> <span class="inlinecode">3</span> <span class="inlinecode">≥</span> <span class="inlinecode"><span class="id" type="var">a</span>*<span class="id" type="var">b</span></span>, in the same way it would
    prove <span class="inlinecode"><span class="id" type="var">u</span></span> <span class="inlinecode">&gt;</span> <span class="inlinecode"><span class="id" type="var">v</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">u</span>+3</span> <span class="inlinecode">≥</span> <span class="inlinecode"><span class="id" type="var">v</span></span>.

<div class="paragraph"> </div>

    Now let's consider a silly little program: swap the first two
    elements of a list, if they are out of order. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">maybe_swap</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">list</span> <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">al</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">a</span> :: <span class="id" type="var">b</span> :: <span class="id" type="var">ar</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">a</span> &gt;? <span class="id" type="var">b</span> <span class="id" type="keyword">then</span> <span class="id" type="var">b</span>::<span class="id" type="var">a</span>::<span class="id" type="var">ar</span> <span class="id" type="keyword">else</span> <span class="id" type="var">a</span>::<span class="id" type="var">b</span>::<span class="id" type="var">ar</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">al</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">maybe_swap_123</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">maybe_swap</span> [1; 2; 3] = [1; 2; 3].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">maybe_swap_321</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">maybe_swap</span> [3; 2; 1] = [2; 3; 1].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
In this program, we wrote <span class="inlinecode"><span class="id" type="var">a</span>&gt;?<span class="id" type="var">b</span></span> instead of <span class="inlinecode"><span class="id" type="var">a</span>&gt;<span class="id" type="var">b</span></span>.  Why is that? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> (1&gt;2). <span class="comment">(*&nbsp;:&nbsp;Prop&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> (1&gt;?2). <span class="comment">(*&nbsp;:&nbsp;bool&nbsp;*)</span><br/>
</div>

<div class="doc">
We cannot compute with elements of <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>: we need some kind of
    constructible (and pattern-matchable) value.  For that we use
    <span class="inlinecode"><span class="id" type="var">bool</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="var">Locate</span> "&gt;?". <span class="comment">(*&nbsp;a&nbsp;&gt;?&nbsp;b&nbsp;:=&nbsp;&nbsp;ltb&nbsp;b&nbsp;a&nbsp;*)</span><br/>
</div>

<div class="doc">
The name <span class="inlinecode"><span class="id" type="var">ltb</span></span> stands for "less-than boolean." 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">Nat.ltb</span>.<br/>
<span class="comment">(*&nbsp;=&nbsp;&nbsp;fun&nbsp;n&nbsp;m&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;S&nbsp;n&nbsp;&lt;=?&nbsp;m&nbsp;:&nbsp;nat&nbsp;-&gt;&nbsp;nat&nbsp;-&gt;&nbsp;bool&nbsp;&nbsp;*)</span><br/>
<span class="id" type="var">Locate</span> "&gt;=?".<br/>
</div>

<div class="doc">
Instead of defining an operator <span class="inlinecode"><span class="id" type="var">Nat.geb</span></span>, the standard library just
    defines the notation for greater-or-equal-boolean as a
    less-or-equal-boolean with the arguments swapped. 
</div>
<div class="code code-tight">

<span class="id" type="var">Locate</span> <span class="id" type="var">leb</span>.<br/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">leb</span>.<br/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">Nat.leb</span>. <span class="comment">(*&nbsp;The&nbsp;computation&nbsp;to&nbsp;compare&nbsp;natural&nbsp;numbers.&nbsp;*)</span><br/>
</div>

<div class="doc">
Here's a theorem: <span class="inlinecode"><span class="id" type="var">maybe_swap</span></span> is idempotent &mdash; that is, applying it
    twice gives the same result as applying it once. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">maybe_swap_idempotent</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">al</span>, <span class="id" type="var">maybe_swap</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>) = <span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">a</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">b</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
What do we do here?   We must proceed by case analysis on
     whether a&gt;b. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">b</span> &lt;? <span class="id" type="var">a</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">a</span> &lt;? <span class="id" type="var">b</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">H<sub>0</sub></span>.<br/>
</div>

<div class="doc">
Now what?  Look at the hypotheses <span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">b</span>&lt;<span class="id" type="var">a</span></span> and <span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span>:</span> <span class="inlinecode"><span class="id" type="var">a</span>&lt;<span class="id" type="var">b</span></span>
      above the line. They can't both be true.  In fact, <span class="inlinecode"><span class="id" type="tactic">omega</span></span>
      "knows" how to prove that kind of thing.  Let's try it: 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">omega</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">omega</span></span> didn't work, because it operates on comparisons in <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>,
      such as <span class="inlinecode"><span class="id" type="var">a</span>&gt;<span class="id" type="var">b</span></span>; not upon comparisons yielding bool, such as <span class="inlinecode"><span class="id" type="var">a</span>&gt;?<span class="id" type="var">b</span></span>.
      We need to convert these comparisons to <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>, so that we can use
      <span class="inlinecode"><span class="id" type="tactic">omega</span></span>.

<div class="paragraph"> </div>

      Actually, we don't "need" to.  Instead, we could reason directly
      about these operations in <span class="inlinecode"><span class="id" type="var">bool</span></span>.  But that would be even more
      tedious than the <span class="inlinecode"><span class="id" type="var">omega_example1</span></span> proof.  Therefore: let's set up
      some machinery so that we can use <span class="inlinecode"><span class="id" type="tactic">omega</span></span> on boolean tests. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Let's try again, a new way: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">maybe_swap_idempotent</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">al</span>, <span class="id" type="var">maybe_swap</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>) = <span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">a</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">b</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
This is where we left off before. Now, watch: 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">blt_reflect</span> <span class="id" type="var">b</span> <span class="id" type="var">a</span>). <span class="comment">(*&nbsp;THIS&nbsp;LINE&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Notice&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">b</span>&lt;<span class="id" type="var">a</span></span>&nbsp;is&nbsp;above&nbsp;the&nbsp;line&nbsp;as&nbsp;a&nbsp;Prop,&nbsp;not&nbsp;a&nbsp;bool.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Now,&nbsp;comment&nbsp;out&nbsp;THIS&nbsp;LINE,&nbsp;and&nbsp;uncomment&nbsp;THAT&nbsp;LINE.&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;bdestruct&nbsp;(b&nbsp;&lt;?&nbsp;a).&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;THAT&nbsp;LINE&nbsp;*)</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;THAT&nbsp;LINE,&nbsp;with&nbsp;<span class="inlinecode"><span class="id" type="var">bdestruct</span></span>,&nbsp;does&nbsp;the&nbsp;same&nbsp;thing&nbsp;as&nbsp;THIS&nbsp;LINE.&nbsp;*)</span><br/>
* <span class="comment">(*&nbsp;case&nbsp;b&lt;a&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">a</span> &lt;? <span class="id" type="var">b</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="tactic">omega</span></span> tactic noticed that above the line we have an
      arithmetic contradiction.  Perhaps it seems wasteful to bring
      out the "big gun" to shoot this flea, but really, it's easier
      than remembering the names of all those lemmas about
      arithmetic! 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
* <span class="comment">(*&nbsp;case&nbsp;a&nbsp;&gt;=&nbsp;b&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">b</span> &lt;? <span class="id" type="var">a</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Moral of this story: When proving things about a program that uses
    boolean comparisons <span class="inlinecode">(<span class="id" type="var">a</span></span> <span class="inlinecode">&lt;?</span> <span class="inlinecode"><span class="id" type="var">b</span>)</span>, use <span class="inlinecode"><span class="id" type="var">bdestruct</span></span>.  Then use
    <span class="inlinecode"><span class="id" type="tactic">omega</span></span>.  Let's review that proof without all the comments. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">maybe_swap_idempotent'</span>:<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span> <span class="id" type="var">al</span>, <span class="id" type="var">maybe_swap</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>) = <span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">a</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">b</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">b</span> &lt;? <span class="id" type="var">a</span>).<br/>
*<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">a</span> &lt;? <span class="id" type="var">b</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
*<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">b</span> &lt;? <span class="id" type="var">a</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab15"></a><h1 class="section">Permutations</h1>

<div class="paragraph"> </div>

 Another useful fact about <span class="inlinecode"><span class="id" type="var">maybe_swap</span></span> is that it doesn't add or
    remove elements from the list: it only reorders them.  We can say
    that the output list is a <i>permutation</i> of the input.  The Coq
    <span class="inlinecode"><span class="id" type="var">Permutation</span></span> library has an inductive definition of permutations,
    along with some lemmas about them. 
</div>
<div class="code code-tight">

<span class="id" type="var">Locate</span> <span class="id" type="var">Permutation</span>. <span class="comment">(*&nbsp;Inductive&nbsp;Coq.Sorting.Permutation.Permutation&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation</span>. <span class="comment">(*&nbsp;&nbsp;:&nbsp;forall&nbsp;{A&nbsp;:&nbsp;Type},&nbsp;list&nbsp;A&nbsp;-&gt;&nbsp;list&nbsp;A&nbsp;-&gt;&nbsp;Prop&nbsp;*)</span><br/>
</div>

<div class="doc">
We say "list <span class="inlinecode"><span class="id" type="var">al</span></span> is a permutation of list <span class="inlinecode"><span class="id" type="var">bl</span></span>",
     written <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>, if the elements of <span class="inlinecode"><span class="id" type="var">al</span></span> can be
     reordered (without insertions or deletions) to get the list <span class="inlinecode"><span class="id" type="var">bl</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">Permutation</span>.<br/>
<span class="comment">(*<br/>
&nbsp;Inductive&nbsp;Permutation&nbsp;{A&nbsp;:&nbsp;Type}&nbsp;:&nbsp;list&nbsp;A&nbsp;-&gt;&nbsp;list&nbsp;A&nbsp;-&gt;&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;perm_nil&nbsp;:&nbsp;Permutation&nbsp;<span class="inlinecode"></span>&nbsp;<span class="inlinecode"></span><br/>
&nbsp;&nbsp;|&nbsp;perm_skip&nbsp;:&nbsp;forall&nbsp;(x&nbsp;:&nbsp;A)&nbsp;(l&nbsp;l'&nbsp;:&nbsp;list&nbsp;A),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;l&nbsp;l'&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;(x&nbsp;::&nbsp;l)&nbsp;(x&nbsp;::&nbsp;l')<br/>
&nbsp;&nbsp;|&nbsp;perm_swap&nbsp;:&nbsp;forall&nbsp;(x&nbsp;y&nbsp;:&nbsp;A)&nbsp;(l&nbsp;:&nbsp;list&nbsp;A),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;(y&nbsp;::&nbsp;x&nbsp;::&nbsp;l)&nbsp;(x&nbsp;::&nbsp;y&nbsp;::&nbsp;l)<br/>
&nbsp;&nbsp;|&nbsp;perm_trans&nbsp;:&nbsp;forall&nbsp;l&nbsp;l'&nbsp;l''&nbsp;:&nbsp;list&nbsp;A,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;l&nbsp;l'&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;l'&nbsp;l''&nbsp;-&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Permutation&nbsp;l&nbsp;l''.<br/>
*)</span><br/>
</div>

<div class="doc">
You might wonder, "is that really the right definition?"  And
    indeed, it's important that we get a right definition, because
    <span class="inlinecode"><span class="id" type="var">Permutation</span></span> is going to be used in the specification of
    correctness of our searching and sorting algorithms.  If we have
    the wrong specification, then all our proofs of "correctness" will
    be useless.

<div class="paragraph"> </div>

    It's not obvious that this is indeed the right specification of
    permutations. (It happens to be true, but it's not obvious!)  In
    order to gain confidence that we have the right specification, we
    should use this specification to prove some properties that we
    think permutations ought to have. 
<div class="paragraph"> </div>

<a name="lab16"></a><h4 class="section">Exercise: 2 stars (Permutation_properties)</h4>
 Think of some properties of the <span class="inlinecode"><span class="id" type="var">Permutation</span></span> relation and write
    them down informally in English, or a mix of Coq and English.
    Here are four to get you started:

<div class="paragraph"> </div>

<ul class="doclist">
<li> 1. If <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>, then <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>.

</li>
<li> 2. If <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>, then <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span>.

</li>
<li> 3. <span class="inlinecode">[1;1]</span> is NOT a permutation of <span class="inlinecode">[1;2]</span>.

</li>
<li> 4. <span class="inlinecode">[1;2;3;4]</span> IS a permutation of <span class="inlinecode">[3;4;2;1]</span>.

</li>
</ul>

<div class="paragraph"> </div>

   YOUR ASSIGNMENT: Add three more properties. Write them here: 
<div class="paragraph"> </div>

 Now, let's examine all the theorems in the Coq library about
    permutations: 
</div>
<div class="code code-tight">

<span class="id" type="var">Search</span> <span class="id" type="var">Permutation</span>. <span class="comment">(*&nbsp;Browse&nbsp;through&nbsp;the&nbsp;results&nbsp;of&nbsp;this&nbsp;query!&nbsp;*)</span><br/>
</div>

<div class="doc">
Which of the properties that you wrote down above have already
    been proved as theorems by the Coq library developers?  Answer
    here:

<div class="paragraph"> </div>


</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_Permutation_properties</span> : <span class="id" type="var">option</span> (<span class="id" type="var">prod</span> <span class="id" type="var">nat</span> <span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Let's use the permutation rules in the library to prove the
    following theorem. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">butterfly</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">b</span> <span class="id" type="var">u</span> <span class="id" type="var">t</span> <span class="id" type="var">e</span> <span class="id" type="var">r</span> <span class="id" type="var">f</span> <span class="id" type="var">l</span> <span class="id" type="var">y</span> : <span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Permutation</span> ([<span class="id" type="var">b</span>;<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>]++[<span class="id" type="var">f</span>;<span class="id" type="var">l</span>;<span class="id" type="var">y</span>]) ([<span class="id" type="var">f</span>;<span class="id" type="var">l</span>;<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>]++[<span class="id" type="var">b</span>;<span class="id" type="var">y</span>]).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;Just&nbsp;to&nbsp;illustrate&nbsp;a&nbsp;method,&nbsp;let's&nbsp;group&nbsp;<span class="inlinecode"><span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span></span>&nbsp;together:&nbsp;*)</span><br/>
&nbsp;<span class="id" type="var">change</span> [<span class="id" type="var">b</span>;<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>] <span class="id" type="keyword">with</span> ([<span class="id" type="var">b</span>]++[<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>]).<br/>
&nbsp;<span class="id" type="var">change</span> [<span class="id" type="var">f</span>;<span class="id" type="var">l</span>;<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>] <span class="id" type="keyword">with</span> ([<span class="id" type="var">f</span>;<span class="id" type="var">l</span>]++[<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>]).<br/>
&nbsp;<span class="id" type="var">remember</span> [<span class="id" type="var">u</span>;<span class="id" type="var">t</span>;<span class="id" type="var">t</span>;<span class="id" type="var">e</span>;<span class="id" type="var">r</span>] <span class="id" type="keyword">as</span> <span class="id" type="var">utter</span>.<br/>
&nbsp;<span class="id" type="tactic">clear</span> <span class="id" type="var">Hequtter</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;Next,&nbsp;let's&nbsp;cancel&nbsp;<span class="inlinecode"><span class="id" type="var">utter</span></span>&nbsp;from&nbsp;both&nbsp;sides.&nbsp;&nbsp;In&nbsp;order&nbsp;to&nbsp;do&nbsp;that,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;we&nbsp;need&nbsp;to&nbsp;bring&nbsp;<span class="inlinecode"><span class="id" type="var">utter</span></span>&nbsp;to&nbsp;the&nbsp;beginning&nbsp;of&nbsp;each&nbsp;list.&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">app_assoc</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">app_assoc</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">app_assoc</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">perm_trans</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">perm_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">utter</span> ++ [<span class="id" type="var">f</span>;<span class="id" type="var">l</span>;<span class="id" type="var">y</span>] ++ [<span class="id" type="var">b</span>]).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">app_assoc</span> <span class="id" type="var">utter</span> [<span class="id" type="var">f</span>;<span class="id" type="var">l</span>;<span class="id" type="var">y</span>]).<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation_app_comm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_app_comm</span>.<br/>
&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">perm_trans</span>.<br/>
&nbsp;2: <span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_app_comm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">app_assoc</span>.<br/>
<span class="id" type="var">Search</span> (<span class="id" type="var">Permutation</span> (<span class="id" type="var">_</span>++_) (<span class="id" type="var">_</span>++_)).<br/>
&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_app_head</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;Now&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">utter</span></span>&nbsp;is&nbsp;utterly&nbsp;removed&nbsp;from&nbsp;the&nbsp;goal,&nbsp;let's&nbsp;cancel&nbsp;<span class="inlinecode"><span class="id" type="var">f</span>;<span class="id" type="var">l</span></span>.&nbsp;*)</span><br/>
&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">perm_trans</span>.<br/>
&nbsp;2: <span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_app_comm</span>.<br/>
&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">perm_skip</span>.<br/>
&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">perm_skip</span>.<br/>
&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">perm_skip</span>.<br/>
<span class="id" type="var">Search</span> (<span class="id" type="var">Permutation</span> (<span class="id" type="var">_</span>::_) (<span class="id" type="var">_</span>::_)).<br/>
&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">perm_swap</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
That example illustrates a general method for proving
  permutations involving cons <span class="inlinecode">::</span> and append <span class="inlinecode">++</span>.
  You identify some portion appearing in both sides;
  you bring that portion to the front on each side using
  lemmas such as <span class="inlinecode"><span class="id" type="var">Permutation_app_comm</span></span> and <span class="inlinecode"><span class="id" type="var">perm_swap</span></span>,
  with generous use of <span class="inlinecode"><span class="id" type="var">perm_trans</span></span>.  Then, you use
  <span class="inlinecode"><span class="id" type="var">perm_skip</span></span> to cancel a single element, or <span class="inlinecode"><span class="id" type="var">Permutation_app_head</span></span>
  to cancel an append-chunk. 
<div class="paragraph"> </div>

<a name="lab17"></a><h4 class="section">Exercise: 3 stars (permut_example)</h4>
 Use the permutation rules in the library (see the <span class="inlinecode"><span class="id" type="var">Search</span></span>,
    above) to prove the following theorem.  These <span class="inlinecode"><span class="id" type="keyword">Check</span></span> commands
   are a hint about what lemmas you'll need. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">perm_skip</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation_refl</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation_app_comm</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">app_assoc</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">permut_example</span>: <span style='font-size:120%;'>&forall;</span> (<span class="id" type="var">a</span> <span class="id" type="var">b</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">Permutation</span> (5::6::<span class="id" type="var">a</span>++<span class="id" type="var">b</span>) ((5::<span class="id" type="var">b</span>)++(6::<span class="id" type="var">a</span>++[])).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;After&nbsp;you&nbsp;cancel&nbsp;the&nbsp;<span class="inlinecode">5</span>,&nbsp;then&nbsp;bring&nbsp;the&nbsp;<span class="inlinecode">6</span>&nbsp;to&nbsp;the&nbsp;front...&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab18"></a><h4 class="section">Exercise: 1 star (not_a_permutation)</h4>
 Prove that <span class="inlinecode">[1;1]</span> is not a permutation of <span class="inlinecode">[1;2]</span>.
    Hints are given as <span class="inlinecode"><span class="id" type="keyword">Check</span></span> commands. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation_cons_inv</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">Permutation_length_1_inv</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">not_a_permutation</span>:<br/>
&nbsp;&nbsp;¬ <span class="id" type="var">Permutation</span> [1;1] [1;2].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Back to <span class="inlinecode"><span class="id" type="var">maybe_swap</span></span>.  We prove that it doesn't lose or gain
   any elements, only reorders them. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">maybe_swap_perm</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">al</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">a</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_refl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">b</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_refl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">a</span>&gt;?<span class="id" type="var">b</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">perm_swap</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Permutation_refl</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Now let us specify functional correctness of <span class="inlinecode"><span class="id" type="var">maybe_swap</span></span>:
    it rearranges the elements in such a way that the first is
    less-or-equal than the second. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">first_le_second</span> (<span class="id" type="var">al</span>: <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">al</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">a</span>::<span class="id" type="var">b</span>::_ ⇒ <span class="id" type="var">a</span> ≤ <span class="id" type="var">b</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">True</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">maybe_swap_correct</span>: <span style='font-size:120%;'>&forall;</span> <span class="id" type="var">al</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;∧ <span class="id" type="var">first_le_second</span> (<span class="id" type="var">maybe_swap</span> <span class="id" type="var">al</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">maybe_swap_perm</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">a</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">al</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">b</span> <span class="id" type="var">al</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">bdestruct</span> (<span class="id" type="var">b</span> &lt;? <span class="id" type="var">a</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Exploration1</span>.<br/>
</div>

<div class="doc">
<a name="lab19"></a><h1 class="section">Summary: Comparisons and Permutations</h1>

<div class="paragraph"> </div>

 To prove correctness of algorithms for sorting and searching,
  we'll reason about comparisons and permutations using the tools
  developed in this chapter.  The <span class="inlinecode"><span class="id" type="var">maybe_swap</span></span> program is a tiny
  little example of a sorting program.  The proof style in
  <span class="inlinecode"><span class="id" type="var">maybe_swap_correct</span></span> will be applied (at a larger scale) in
  the next few chapters. 
<div class="paragraph"> </div>

<a name="lab20"></a><h4 class="section">Exercise: 2 stars (Forall_perm)</h4>
 To close, a useful utility lemma.  Prove this by induction;
  but is it induction on <span class="inlinecode"><span class="id" type="var">al</span></span>, or on <span class="inlinecode"><span class="id" type="var">bl</span></span>, or on <span class="inlinecode"><span class="id" type="var">Permutation</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span> <span class="inlinecode"><span class="id" type="var">bl</span></span>,
  or on <span class="inlinecode"><span class="id" type="var">Forall</span></span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">al</span></span>  ? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">Forall_perm</span>: <span style='font-size:120%;'>&forall;</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">f</span>: <span class="id" type="var">A</span> → <span class="id" type="keyword">Prop</span>) <span class="id" type="var">al</span> <span class="id" type="var">bl</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">Permutation</span> <span class="id" type="var">al</span> <span class="id" type="var">bl</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Forall</span> <span class="id" type="var">f</span> <span class="id" type="var">al</span> → <span class="id" type="var">Forall</span> <span class="id" type="var">f</span> <span class="id" type="var">bl</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

  
</div>
</div>



</div>

</body>
</html>